\begin{tabbing}
R{-}pre{-}init($i$;${\it ds}$;${\it init}$;$a$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=@$i$ \=precondition for $a$(v:$T$):\+\+
\\[0ex]$P$ State(${\it ds}$) v
\-\\[0ex]$\oplus$ $\oplus$$x$$\in$fpf{-}domain(${\it ds}$).@$i$ $x$ initially ${\it init}$($x$):${\it ds}$($x$)
\-
\end{tabbing}